\chapter{Introduction}

This dissertation studies 
calculi 
%the theory of abstract languages 
for \emph{higher-order concurrency}, 
and focuses on %two of their fundamental aspects: 
their
\emph{expressive power} and \emph{decidable properties}.
Our thesis is that a \emph{direct} and \emph{minimal} approach 
to the 
expressiveness and decidability 
of higher-order concurrency is 
both 
\emph{necessary}
and 
\emph{relevant},
given 
the emergence of higher-order process calculi with \emph{specialized constructs} and 
the inconvenience (or non-existence) of first-order representations 
for such constructs.

%As a consequence, the 


%We motivate the present work by 
%of \emph{global} and \emph{ubiquitous} computing environments, 
%and 



\section{Context and Motivation}
The challenging nature of \emph{concurrent systems} is no longer a novelty for computer science.
In fact, by now there is a 
consolidated understanding on how 
%on the ways in which 
concurrent behavior departs from sequential computation.
Based on pioneering developments by Hewitt, Milner, Hoare, and others, 
%This has allowed, during 
the last three decades have witnessed a remarkable progress on the formulation 
of foundational theories of concurrent processes;  
notions such as \emph{interaction} and \emph{communication} 
are 
%clearly seen to 
widely accepted to 
be intimately related to \emph{computing} at large.
%be central to understand modern computing systems and their intrinsic phenomena.
Given the wealth of abstract languages, theories, and application areas that 
have emerged from this progress, it is fair to say that 
\emph{concurrency theory} is  no longer in its infancy.

%As such, we find ourselves in a place where in which 
%consolidating the development achieved so far appears to be more 
%theories call for consolidation.

%This %``early maturity'' 
%stage
This development 
of concurrency theory coincides with 
the transition towards 
\emph{global ubiquitous computing} we witness nowadays.
Supported by a number of technological advances
---most notably, 
the availability of cheaper and more powerful processors, 
the increase in flexibility and power of communication networks,
and the widespread consolidation of the Internet---
global ubiquitous computing (\guc, in the sequel) %refers essentially to 
is a broad term that refers to 
computing over massively networked, dynamically reconfigurable infrastructures 
that interconnect
heterogeneous collections of computing devices.
%that support a growing range of activities 
%(see, e.g. \citep{Milner06}).
As such, systems in \guc represent the natural evolution of traditional distributed systems, 
and distinguish 
from these in aspects such as
\emph{mobility}, 
\emph{network-awareness}, 
and
\emph{openness} on which we comment next.
%We find it convenient to elaborate on some of these aspects, namely 

%\emph{Mobility} can be interpreted in many ways, depending on the level of abstraction.
Nowadays we find \emph{mobility} in \emph{devices}
that move in our physical world while performing diverse kinds of computation
(mobile phones, laptops, PDAs), as well as in  
%communication 
\emph{objects} travelling across communication networks 
(SMSs, structured data as XML files, snippets of runnable code, software agents).
Sustained advances in bandwidth growth and network connectivity 
have broaden the range of feasible communications; 
as a result, communication objects 
not only 
exhibit now an increasingly complex structure 
but also an autonomous %and self-contained 
nature. 
%that is independent of the context in which they coexist or execute. 
This evolution in the nature of communication objects 
can be seen 
in a number of applications these days:

% tion objects travelling across communication networks (SMSs, structured data as XML ﬁles,
% snippets of runnable code, software agents). Sustained advances in bandwidth growth and
% network connectivity have broaden the range of feasible communications; mobile communica-
% tion arises now from many diﬀerent kinds of devices, and involves forms of interaction based on
% the distribution of complex communication objects. As a matter of fact, nowadays we witness
% the emergence of a number of network-dependent technologies and paradigms that feature
% interaction patterns that rely heavily on connectivity. Some examples include:


\begin{description}
 \item[Distribution of digital content.]
%Nowadays one can 
It is 
becoming increasingly popular 
to buy the right to download  
digital content (music, video, books)
from online stores directly to 
personal computers or  mobile devices. % of many different kinds.
Here the communication objects are the (pieces of) multimedia files that are 
transmitted from the online store to the customer; 
these are files in standardized media formats and hence self-contained to a large extent.
%It is easy to see that 
%this scheme of content distribution depends on the 
%possibility of transmitting large files reliably over the Internet.

\item[\emph{Plug-ins} (or \emph{add-ons}).]
Plug-ins are self-contained programs that integrate within applications (e.g. web browsers, email clients) 
with the purpose of inserting, removing, or updating functionalities at runtime.
For instance, 
plug-ins 
in web browsers
have made possible 
a transition from data mobility to code mobility:
rather than submitting data to a web service and getting results, 
the model is to \emph{download} the required behavior 
(e.g. a snippet of JavaScript code)
and \emph{apply} it to data which may be local or remote. 
Similarly,  most tools for software update are in fact 
 small helper applications available online, ready to be downloaded; 
once installed, they 
obtain information on the current configuration of the system 
and use it to retrieve the most appropriate update from some application server.
%Both plug-ins and tools for software update rely on the fact that 
%objects of considerable size can be transmitted in a reliable way. 

\item[Service-oriented Computing.] 
\emph{Services} are software artifacts which 
can be accessed, manipulated, structured into complex architectures, and 
distributed in wide area networks such as the Internet. 
Services are the building blocks in service-oriented computing, an approach to distributed applications
that has received much attention in recent years.
Forms of \emph{service mobility} are most natural to service-oriented architectures
that define workflows involving services which cannot be determined statically before
execution. As such, these services must be found and integrated at run time.
The behavior of such architectures thus depends on correct, reliable forms of service/code
mobility.
\end{description}


%(think of, for instance, the multimedia/interactive content available for mobile phones).
% are 
% %the small 
% applications for software update: 
% these are small programs which
% once downloaded into a user's system, 
% examine its current configuration so as to retrieve from the Web the newest version
% that is compatible with such a configuration.



%A commonality to n
%Network-dependent technologies 
%Forms of m
%Mobility of complex communication objects 
%as in the examples above 
%is that they 
In general, 
mobility 
cannot abstract from the \emph{locations} 
%in which 
of the moving entities 
(computing devices, communication objects). % are placed.
For instance, in the service-oriented computing scenario just sketched,
it is crucial to be able to tell
\emph{where} a requested service is (e.g. in the service provider, in the requester, in transit)
as such information entails a different behavior for the system.
A location can be as concrete as the wireless network a PDA connects to, 
%or can be determined by more abstract or logical notions, such as, e.g., 
or as abstract as 
the administrative domains in which wide area networks are usually partitioned. 
%Independently of their actual meaning, 
A commonality here is the 
%in global and ubiquitous environments often there is a 
reciprocal relationship between locations and mobility, as 
(the behavior of) a mobile entity and its surrounding environment (determined by its location) 
might have direct influence on each other.
This can be seen, for instance, in %Examples include %Network-awareness manifests itself in, for instance, %from a physical level, 
the relationship between network bandwidth 
and the quality of service available to mobile devices;  
%in the websites which dynamically change their content and services depending on the country in which they are accessed; 
in the %online services and content 
websites 
that change depending on the country in which they are accessed; 
in the actions of network reconfiguration triggered by high peaks of user activity.
%the administrative domains of a corporate network which define 
%security permissions tailored to 
%each moving entity in the organization (files, devices, people).
This phenomenon is sometimes referred to as \emph{network-awareness}:
it can be seen to embody
 %and, as the previous examples suggest, 
%it manifests itself at multiple levels. % within global computing environments.
%at the heart of it
%network-awareness  there is 
a notion of \emph{structure} that 
not only underlies mobile behavior but that often determines it.
%and is inherent to it. 

The \emph{openness} of modern computing environments results from the understanding 
that systems in \guc 
%ubiquitous and global computing systems 
are built as 
very large collections of loosely coupled, heterogeneous components. 
These components might not be known a priori; 
unknown or partially specified components 
could enter and leave the system at will. 
In general, an open system should allow 
to add, suspend, update, relocate, and remove entire components transparently.
From a global point of view, open systems are seldom meant to terminate; 
as such, their overall behavior must abstract from 
changes on the local state of its components, and in particular from their malfunction. 
Hence, forms of \emph{dynamic system reconfiguration}, with varying levels of autonomy,
are most natural within 
models of open systems.
It is worth pointing that 
openness is closely related to mobility and network-awareness 
in that not only complete components might move across the predefined structure of the system, 
but also it might occur that such a structure is reconfigured as a result of the interactions of mobile components.
This is the case of, for instance, a running component which disconnects from one location and
later on reconnects to some other location. 

%Global and ubiquitous computing environments 
Systems in \guc 
therefore represent a challenge for computer science in general, 
and for concurrency theory in particular. 
As we have seen, such environments feature complex forms of concurrent behavior that 
go way beyond the (already complex) interaction patterns present in traditional distributed systems. 
The challenge therefore consists in the formulation of 
foundational theories to cope with the 
features of modern computing environments. 
% One of the most influential foundations developed  
% within concurrency theory 
% for reasoning on the behavior of concurrent systems is
% represented by \emph{process calculi}: ``small'' formalisms with a handful of operators
% intended to capture the essential features of the systems of interest.

We believe that in this context 
\emph{higher-order concurrency} has much to offer.
In fact, process-passing communication as available in higher-order process calculi 
is closely related to the aspects of mobility, network-awareness, and openness 
%as motivated above for 
discussed for 
%global and ubiquitous computing environments.
\guc.
The communication of objects with complex structure
%as in modern incarnations of mobility  %just discussed
can be neatly represented 
in higher-order process calculi
by the communication  of \emph{terms} of the language.
As in the first-order case, extensions of higher-order process calculi
with constructs for %representing 
network-awareness are natural; 
process communication adds the possibility of 
describing
richer and more realistic interaction patterns between different computation loci. 
Furthermore, higher-order communication allows 
to consider 
%is convenient to models of open systems 
%based on 
autonomous, self-contained 
software artifacts ---such as components, services, or agents---
as \emph{first-class objects} which can be moved, executed, manipulated.
This allows for 
%achieving models of open systems which allows for 
clean and modular descriptions of open systems and their behavior.
%and %facilitates the definition %of specialized operators and 
%reasoning techniques.

At this point it might be clear that higher-order communication 
arises in abstract languages for 
\guc
%global and ubiquitous scenarios
in the form of \emph{specialized constructs} that go beyond mere process communication.
%Such constructs exploit the first-class status processes have in higher-order concurrency
%for the purposes of some particular application.
Instances of such constructs include 
forms of \emph{localities} that lead to involved process hierarchies featuring complex communication patterns;
operators for \emph{reflection} that allow to observe and/or modify process execution at runtime;
%constructs for the \emph{suspension} (and reactivation) of process execution;
sophisticated forms of \emph{pattern matching} or 
\emph{cryptographic operations} 
used %begin by noticing that the 
over terms representing messages
or semi-structured data.
%as part of input operations.

The wide range 
and inherent complexity 
of the higher-order interactions that underlie 
these specialized operators 
cast serious doubts 
on the convenience of studying
the theory of higher-order concurrent languages featuring such operators
by means of first-order representations. 
%as to whether the traditional approach of representing higher-order constructs into first-order ones is the right one. 
Based on 
this insight,
%all the above, 
in this dissertation we shall argue  
%higher-order concurrency is relevant in its own right. 
%More precisely, we shall argue 
that foundational studies for higher-order process calculi
must be undertaken \emph{directly} on them and exploit their peculiarities.
This is particularly critical for those issues that have remained unexplored in the theory of higher-order concurrency.
We shall concentrate on two of such issues, namely  
\emph{expressiveness} and \emph{decidability}, two closely interwoven concerns in process calculi at large. 



% Given the long tradition on process calculi for mobile processes, 
% one could expect such calculi to provide a ``roadmap''
% for % on which 
% the development of theories for 
% global and ubiquitous computing at large. % can start from.
% While it would be unrealistic to expect new theories to
% arise as mere extensions of well-established calculi, it is reasonable to expect 
% research on calculi for mobile processes to \emph{guide} new developments: 
% the experience accumulated in the development of 
% existing abstract languages and their reasoning techniques could give hints 
% on sensible issues to 
% consider when developing new ones.
% It is therefore reasonable to review calculi for mobility 
% in the light of the global and ubiquitous environments motivated above.

\section{First-Order and Higher-Order Concurrency}
In this section we first comment on the relationship between first-order and higher-order concurrency.
Then, we give intuitions on Sangiorgi's representability result 
of higher-order into first-order concurrency, and argue that it 
does not carry over to higher-order languages with specialized constructs.
As compelling example, we illustrate the case of a higher-order process calculus with 
a very basic form of localities. 
% Then, we briefly comment on expressiveness and decidability in process calculi, and 
% give a broad overview on the previous works for higher-order process calculi.



\paragraph{Two Kinds of Mobility.}
Broadly speaking, mobility has arisen in calculi for concurrency in essentially 
two kinds: \emph{link} and \emph{process} mobility.
In the first kind it is \emph{links} that move in an abstract  space of linked processes, 
whilst in the second kind it is \emph{processes} that move \citep{SaWabook}.
By far, link mobility has attracted most of the attention of the research community in process calculi.
In the $\pi$-calculus \citep{MilnerPW92a,SaWabook} 
---arguably the most influential process calculus---
link mobility is achieved by means of \emph{name-passing}. 
%this can be appreciated in the 
While the impact of the $\pi$-calculus 
can be appreciated in the numerous efforts devoted to study its theory, variants, and 
applications, its significance 
is strongly related to the unifying view it provides to explain
otherwise unrelated models and paradigms %and phenomena 
such as, e.g., the $\lambda$-calculus \citep{Milner92,San923},
concurrent object-oriented programming \citep{Walker95},
and structured communication \citep{HondaVK98}.
%As a consequence, 
It is therefore no surprise that 
\emph{first-order concurrency} based on the communication of links 
is the predominant paradigm in process calculi for mobility. 

In comparison, process calculi for \emph{higher-order concurrency}
have attained much less attention. 
%In an initial stage, h
Higher-order process calculi emerged first as concurrent extensions of functional languages
(see, e.g., \citep{Boudol89,Nielson89}).
As a matter of fact, higher-order process calculi are inspired by, and formally close to, the
$\lambda$-calculus, whose basic computational step --- $\beta$-reduction --- involves term instantiation.\footnote{Probably as a consequence of this, 
the appellation \emph{higher-order} is often used to refer to the exchange of values 
that might contain terms of the language, i.e., processes.
%Remarkably, %such an exchange is meant to take place in a \emph{non-linear} manner: 
Also intrinsically related with the  appellation higher-order is the 
\emph{non-linear} character of process mobility in higher-order process calculi:
upon reception, received processes can be freely copied, or even discarded.
This is one of the points of contrast between higher-order process calculi
and calculi for mobility such as Ambients \citep{CardelliG00} and its several variants, %and Seal \citep{CastagnaVN05}, 
in which processes can move around but 
\emph{cannot} be copied or discarded, i.e., they feature \emph{linear} process mobility.
For this reason, in what follows we \emph{do not} consider calculi such as Ambients as higher-order process calculi.} 
Later on, as a way of studying
forms of code mobility and mobile agents,
a number of process calculi extended with process-passing features were put forward; 
examples include CHOCS \citep{Tho89}, Plain CHOCS \citep{Tho93}, 
and the  Higher-Order $\pi$-calculus \citep{San923}, which 
were intensely studied in the early 1990s. 
Although that period witnessed 
%In that period, 
remarkable progresses 
on the theory of higher-order process calculi (most notably, on the development of their behavioral theory), 
%However, 
a number of fundamental issues 
were not addressed. % unexplored for them. 
Some of such issues still remain %largely 
unexplored;
this is the case of expressiveness and decidability, central to this  dissertation.


The contrast in the attention that each paradigm has received is certainly not a coincidence. 
We believe it can be explained by the introduction of what is probably the most prominent 
result for higher-order process calculi:
in the context of the %(Higher-Order) 
$\pi$-calculus, 
\cite{San923} showed that the higher-order paradigm is \emph{representable} into the first-order one
by means of a rather elegant translation, in which the
communication of a process is modeled as the communication of a pointer that can activate
as many copies of such a process as needed. 
Crucially, such a translation is \emph{fully-abstract}
with respect to barbed congruence, the form of contextual equivalence used in concurrency theory.
Hence, the behavioral theory  
from the 
first-order setting can be readily transferred 
to the higher-order one.
By demonstrating that the higher-order paradigm only adds modeling convenience, 
this result greatly contributed to consolidate the $\pi$-calculus as a basic formalism for concurrency. 
It also appears to have contributed to %reduce the 
a decline of 
interest in %(the theoretically more involved) 
 formalisms for higher-order concurrency.
In our view, Sangiorgi's representability result was 
so 
conclusive at that time that it indirectly 
put forward the idea that 
his translation could be adapted to represent 
\emph{every} kind of higher-order interaction. 
%We are of the opinion that this %generated a generalized 
This misconception 
%on the nature of higher-order communication 
%---a misconception that 
seems to persist nowadays, even if, as we shall see, 
%It is in fact a misconception for 
it has been shown that for higher-order process calculi 
with little more than process communication, translations into some first-order language 
---as in Sangiorgi's representability result--- are 
unsatisfactory 
%difficult to handle 
or do not exist. 

%

%At this point it is most useful to 
%We 
\paragraph{Sangiorgi's Representability Result.}
Let us give an intuitive overview of Sangiorgi's representability result of higher-order $\pi$-calculus
into the (first-order) $\pi$-calculus, as presented in \citep{San923}. 
The discussion here will be informal: our focus will be on rough intuitions rather than on technicalities. 
Formal details and extended explanations are deferred to Chapter \ref{chap:prelim}. 

Sangiorgi's translation of higher-order into first-order 
$\pi$-calculus 
can be presented as follows.
Let us use $P, Q, R, M, N, \ldots$ to range over processes.
Assume that %a higher-order process calculus in which 
$\outC{a}\langle P \rangle. Q $ represents the output of process $P$ on name (or channel) $a$, 
with continuation $Q$.
%and then behaves as $Q$. 
The higher-order input action $a(x).P$ expects a process value on name $a$
and, upon reception of a process $R$ in the bound variable $x$, 
it behaves as the process $P$ in which all free occurrences of $x$ have been 
substituted with $R$. Constructs for parallel composition $\parallel$, 
non-deterministic choice $+$, 
name restriction $\nu r\, P$, process replication $!P$, and inaction $\nil$
are assumed as expected. 
The \emph{reaction rule}
\[
(a(x).M + M') \parallel (\outC{a}\langle R \rangle.N + N') \arro{~~} M \sub R x \parallel N  \, .
\]
defines the behavior of higher-order processes independently of its environment.

As an example, consider the higher-order process 
\begin{equation}\label{exam:fproc}
 P \eqdef \outC{a}\langle \outC{b} \langle R\rangle.\nil \rangle. \nil \parallel a(x).x \parallel b(y).y
\end{equation}

for which it holds that
\begin{eqnarray*}
 P & \arro{~~}  & \outC{b} \langle R\rangle.\nil  \parallel b(y).y \\
 & \arro{~~}  & R \, .
\end{eqnarray*}

 
We consider now the translation of higher-order processes into the $\pi$-calculus. 
As mentioned before, it represents process passing by means of \emph{reference passing}.
Let $\encp{\cdot}{}$ be the mapping from the higher-order $\pi$-calculus into the $\pi$-calculus defined as
\begin{eqnarray*}
 \encp{\outC{a}\langle P \rangle. Q }{} & = & (\nu m )\, \outC{a}\langle m \rangle.(\encp{Q}{} \parallel !m. \encp{P}{}) \quad \mbox{with~} m \notin \fn{P,Q}\\
\encp{a(x).R}{} & = & a(x).\encp{R}{}  \\
\encp{x}{}& = & \outC{x} 
\end{eqnarray*}
and that is a homomorphism for the other constructs. 
Intuitively, the communication of a process $P$ is represented by the communication of a 
unique name $m$ that is used by the recipient to \emph{trigger} as many copies of $P$ as required. 
Now consider the translation of $P$ in (\ref{exam:fproc}); it is given as follows, with $m, n$ fresh in $R$, 
\begin{eqnarray*}
 \encp{P}{} & = &   (\nu m )\, \outC{a}\langle \outC{m} \rangle.(\nil \parallel !m. \encp{\outC{b} \langle R\rangle.\nil}{}) 
\parallel a(x).\outC{x} \parallel b(y).\outC{y} \\
& = & (\nu m) \, \outC{a}\langle \outC{m} \rangle.(\nil \parallel !m.(\nu n )\, \outC{b} \langle n \rangle.( \nil \parallel !n. \encp{R}{}) ) \parallel a(x).\outC{x} \parallel b(y).\outC{y}
\end{eqnarray*}
 we then have
 \begin{eqnarray*}
 \encp{P}{} & \arro{~~} & 
(\nu m) \, (!m.(\nu n) \, \outC{b} \langle n \rangle. (\nil \parallel !n. \encp{R}{}) \parallel  \outC{m}) \parallel b(y).\outC{y} \\ 
& \arro{~~} & (\nu m) (\nu n) \, (\outC{b} \langle n \rangle.(\nil  \parallel !n. \encp{R}{}) \parallel !m.(\nu n) \, \outC{b} \langle n \rangle. (\nil \parallel !n. \encp{R}{})) \parallel b(y).\outC{y} \\
& \arro{~~} & (\nu m) (\nu n) \, (!n. \encp{R}{} \parallel !m.(\nu n) \, \outC{b} \langle n \rangle. (\nil \parallel !n. \encp{R}{}) \parallel \outC{n}) \\
& \arro{~~} & (\nu m) (\nu n) \, (\encp{R}{} \parallel !n. \encp{R}{} \parallel !m.(\nu n) \, \outC{b} \langle n \rangle. (\nil \parallel !n. \encp{R}{})) \\
 %& \arro{~~} & \nu n \, (!n. \encp{R}{} \parallel \outC{n}) \\ 
&  \sim & \encp{R}{} 
\end{eqnarray*}
where $\sim$ stands for a relation that allows to disregard behaviorally irrelevant processes.

\paragraph{When First-Order Is Not Higher-Order.}
The above example should be sufficient to understand how 
process mobility is realized by means of reference passing
in Sangiorgi's translation.
Indeed, the movement of processes is represented as the movement of names that \emph{refer} to processes.
At this point it is useful to quote
\cite{CardelliG00} 
who, 
when introducing the Ambient calculus, 
criticize a reference-based approach to mobility:

\begin{quote}
There is no clear indication that processes themselves move. 
For example, if a channel crosses a firewall (that is, if it is communicated to a process meant to represent a firewall), 
there is no clear sense in which the process has also crossed the firewall. 
In fact, the channel may cross several independent firewalls, but a process could not be in all those places at once.
\end{quote}

% As a matter of fact, \cite{CardelliG00} take this shortcoming as 
% a compelling motivation to develop the Ambient calculus,
% one of the first calculi for global computing. 
% \emph{movement} and \emph{ambients} ---hierarchical representations of administrative domains--- 
% are prominent notions. 

As a matter of fact, 
what this remark reveals is the following: 
when process mobility is to be considered in conjunction with notions 
of observable behavior that explicitly account for the location in which behavior takes place, 
the reference-passing approach for mobility is \emph{inadequate} to capture process movement.
Translations such as 
Sangiorgi's %translation is 
are 
therefore \emph{not robust enough}
in the context of explicit notions of locality, such as the required by 
in the modelling of network-aware systems.

Let us elaborate on this point by means of an example. 
Consider the higher-order process
\begin{equation}\label{examp:proc}
 P \eqdef \outC{a}\langle T \rangle. Q \parallel a(x).(x \parallel x) \, .
\end{equation}

It is easy to see that via a synchronization on $a$, $P$ is able to produce two copies of $T$, 
running in parallel with the continuation $Q$, i.e.
\[
 P \arro{~~} Q \parallel T \parallel T \,. 
\]
Now suppose we extend our higher-order calculus with a basic form of localities.
More precisely, let us assume that processes are of the form $\{P\}_l$ which intuitively represents the process $P$ executing 
in the computation locus $l$. 
The reaction rule given before is extended accordingly;
it allows interactions between complementary actions in two ---possibly different--- localities:
\[
\{a(x).M + M'\}_m \parallel \{\outC{a}\langle R \rangle.N + N'\}_n \arro{~~} \{M \sub R x \}_m \parallel \{N\}_n  \, .
\]

Let us consider $P'$, the located version of $P$ in (\ref{examp:proc}).
Process $P'$ involves two different localities $s$ and $r$ for sender and receiver processes, respectively:
\[
 P' \eqdef \{ \outC{a}\langle T \rangle. Q \}_s \parallel \{  a(x).(x \parallel x)\}_r \, .
\]
The behavior of $P'$ is essentially the same of $P$, % with the additional level of detail given by the locations:
except for the fact that 
$T$ is associated to location $r$. 
Intuitively, this represents the \emph{movement} of $T$ 
in the space of locations both $s$ and $r$ belong to:
%from location $s$ to location $r$:
\[
 P' \arro{~~} \{Q\}_s \parallel \{T \parallel T\}_r \,. 
\]
Indeed, we now have an observable behavior of the system that is finer in that we are now able to tell
not only that $Q$ executes in parallel with two copies of $T$, but also 
that $Q$ executes in location $s$ whereas that
$T \parallel T$ executes in location $r$.
Let us consider the first-order representation of $P'$ given by the extension of
Sangiorgi's translation to the located case.
(Without loss of generality we can assume that the translation $\encp{\cdot}{}$ 
is homomorphic also with respect to locations, i.e.
$\encp{\{P\}_l}{} =  \{ \encp{P}{} \}_l$.) This way, we have 
\begin{eqnarray*}
\encp{P'}{} & = & \{(\nu m)\, \outC{a}\langle m \rangle.(\encp{Q}{}  \parallel !m. \encp{T}{} )\}_s \parallel \{ a(x).(\outC{x} \parallel  \outC{x})\}_r \\
& \arro{~~} & (\nu m)\, (\{\encp{Q}{}  \parallel !m. \encp{T}{} \}_s \parallel \{ \outC{m} \parallel  \outC{m}\}_r) \\
& \arro{~~} & (\nu m)\, (\{\encp{Q}{}  \parallel \encp{T}{}  \parallel !m. \encp{T}{} \}_s \parallel \{ \outC{m} \}_r) \\
& \arro{~~} \sim & \{\encp{Q}{}  \parallel \encp{T}{}  \parallel \encp{T}{} \}_s \parallel \{ \nil \}_r
\end{eqnarray*}
which is certainly unsatisfactory under any reasonable notion of behavioral equivalence 
with explicit locations since, 
unlike the source term, 
process $\encp{T \parallel T}{}$ is executed in location $s$.
It is clear that what moved in the translation was a pointer to the copies, rather than the processes themselves. 

The morale of this example is that while translations such as Sangiorgi's are satisfactory 
in the case of ``basic'' higher-order languages, this is  not necessarily the case for 
higher-order process calculi with specialized constructs, such as the ones required in global and ubiquitous computing scenarios.
It is in this sense that we claim that Sangiorgi's representability result induced 
a generalized misconception, both on the nature of higher-order communication and on the
applicability of the translation. 
This is certainly not an original insight; 
as a matter of fact, \cite{SaWabook} comment on this issue, 
remarking on the potentially dangerous effects some other operators could have in 
Sangiorgi's translation. 
% for handling higher-order languages
%with little more than process communication has been observed before: 
%Apart from the already mentioned remark in \citep{CardelliG00}, the same phenomenon
%Concrete consequences of such effects 
%has been studied by 
\cite{VivasD98} and \cite{VivasY02} 
have studied such effects in the case of higher-order languages
involving dynamic binding. % (see Chapter \ref{chap:prelim} for further discussions).
Also, the nature of the \emph{passivation} operators introduced in 
\citep{HilBun04,SchmittS04}
to represent the \emph{suspension} of executing processes 
---as required in, e.g., forms of dynamic system reconfiguration--- 
strongly suggests that they are not 
representable into some first-order setting. 
All these works thus provide compelling evidence of the need of developing the theory of 
higher-order process calculi \emph{directly on them}, without going through intermediate translations. 

% \subsection{Complex Communication Objects Matter}
% Up to now we have argued for a direct approach to higher-order concurrency, 
% based both on the shortcomings of an indirect approach that relies on first-order concurrency
% and on some of the features of global and ubiquitous computing environments. 
% There is another perspective for justifying this direct approach that is worth commenting on:
% the role of higher-order concurrency as abstract languages for representing complex communication objects.
% THINK ABOUT THIS.


\section{This Dissertation}
This dissertation studies expressiveness and decidability issues
in higher-order concurrency.
The research is centered around a \emph{core calculus} 
for higher-order concurrency in which only
the operators strictly necessary to obtain higher-order communication are retained. 
Next, we give an overview to expressiveness and decidability in concurrent languages in general,
and in higher-order concurrency in particular. 
Then, we elaborate on the approach we shall follow in our research.
Finally, we comment on the contributions and structure of the dissertation.


\subsection{Expressiveness and Decidability in Higher-Order Concurrency}
An important criterion for assessing the significance of a paradigm is its \emph{expressiveness}.
Expressiveness studies are concerned with 
formal assessments of the 
\emph{expressive power} of
a language or family of languages. 
The precise meaning of ``expressive power''
depends on the purpose, and several suitable definitions are possible.
At the heart of all of them, however, 
is the notion of \emph{encoding}:
a map from the terms of a \emph{source language} 
into those of a \emph{target language}, subject to a set of  \emph{correctness criteria}.


The quest for a unified definition of encoding
---in particular, a set of correctness criteria that a \emph{good encoding} should enforce---
has been a matter of research for some time now, and concrete proposals have been put forward.
In spite of this, there is yet no general agreement on such a definition.
In our view, a single, all-embracing definition of encoding is unlikely to  exist, essentially because 
expressiveness studies may have many different purposes, and may be carried out over
concurrent languages of a very diverse nature.
%For instance, 
This way,
the set of criteria required in the definition of 
a taxonomy aimed at \emph{relating} different  process calculi 
%While efforts towards a deeper understanding 
%of the expressive power of process calculi 
%are of great interest in themselves for they 
%might help to understand the constructs of a given language and/or 
%sheds light on the \emph{relationships} between them, %different calculi, 
should be different from, for instance,
 the criteria 
required when the interest is on 
\emph{transferring} reasoning principles from one language to another. 
Indeed, whereas in the latter case 
the definition of encoding should impose rather strict criteria on 
the relationship between equivalent
terms in both source and target languages, in the former case
the adopted definition 
%a notion of encodings 
could well enforce milder forms of correspondence between equivalent terms, 
%focus more on 
and/or
consider criteria oriented at capturing precise aspects of the 
relationships of interest. 
Hence, differences between the two sets of criteria do not mean
one is better than the other; they just reflect the different motivations
underlying the respective expressiveness studies.
Nevertheless, considering the ``quality'' of an encoding is still interesting because,
as we shall see, there is a direct relationship between the precise definition of encoding
and the significance of the results obtained with it.
%adopted in a given expressiveness study and the significance of the results obtained from the study;
We treat this issue in length in Chapter \ref{chap:prelim}.
%In this sense, the set of criteria adopter in either case 




As hinted at above, expressiveness 
has been little studied
%remains a largely unexplored issue 
for higher-order process calculi.
Most previous works address issues of \emph{relative} expressiveness: 
higher-order  calculi (both sequential and concurrent) have been compared with first-order calculi, but mainly as a way of investigating the expressiveness of the $\pi$-calculus  and similar formalisms.
In addition to the representability result in \citep{San923}, the expressiveness of higher-order process calculi was studied in \citep{San96int}, where variants of the $\pi$-calculus with different degrees of \emph{internal mobility} are related to typed variants of the Higher-Order $\pi$-calculus. %The expressive power of process passing is analyzed 
Interestingly, this work presents
%by presenting 
encodings of (variants of) the $\pi$-calculus into  %typed higher-order calculi. This is remarkable in that the target language are 
\emph{strictly} higher-order process calculi, 
i.e., calculi in which only pure process passing is allowed and no name-passing is present.
The only other result on the expressiveness of pure process passing we are aware of
is \citep{BundgaardHG06}, where an encoding of the $\pi$-calculus into Homer
---a higher-order process calculi with locations \citep{HilBun04}--- is presented.
Encodings of variants of the $\pi$-calculus into
the Higher-Order $\pi$-calculus were first given in \citep{San96int} and later consolidated in
\citep{SaWabook}, where the abstraction mechanism of the higher-order $\pi$-calculus 
%(it needs $\omega$-order abstractions) 
is exploited.
\cite{Tho90} and \cite{Xu07} 
have proposed encodings of $\pi$-calculus
into Plain CHOCS. These encodings make essential use of the
relabeling operator of Plain CHOCS. 
% Another strand of  work on expressiveness (see, e.g., \citep{PhillipsV08})
% %\cite{PhillipsV04,BugliesiCMS05,BundgaardHG06}
% %\finish{Check these cites}
% %  somehow 
% % related to higher-order calculi 
% has looked at   calculi for distributed systems and compared
%  different  primitives for  migration and movement  of  processes  (or entire
%  locations), which can be seen as higher-order constructs.

The expressiveness of concurrent languages 
is closely related to
\emph{decidability issues}. 
Given a concurrent language, 
it is legitimate to ask whether or not its expressive power is related to the decidability of some property of interest.
Examples include properties related with 
\emph{behavioral equivalences} (e.g. strong bisimilarity),
%properties related to process 
\emph{termination of processes} (e.g. convergence), 
and %properties over 
graph-like structures (e.g. reachability and coverability). 
An appealing question here is ``what is the most expressive fragment of the language in which the property is decidable?''
There is a trade-off between expressiveness and decidability: 
most interesting decision problems are generally undecidable for very expressive languages. 
Hence, given a process calculus and some property of interest, 
a common research direction is 
%singling out the precise construct(s) 
identifying the largest sub-calculus for which the property is decidable. 
%that cause causing a \emph{separation} between decidability and undecidability, 
Studies dealing with the interplay of expressiveness and decidability are relevant in 
that they provide support for \emph{verification}:
they %decidability of some property 
might pave the way for the implementation of tools, or 
%They can also 
provide insights on the aspects that might be sensible for verification purposes.

%Therefore, identifying expressive language fragments with decidable properties is both challenging 
%and necessary. 

Studies of decidable properties for higher-order process calculi are scarce.
The only work we are aware of is \citep{BundgaardGHH09}, in which 
the interest is on the decidability of barbed bisimilarity in the context 
of Homer. %, a higher-order calculus with locations 




\subsection{Approach}
We shall follow a \emph{direct} and \emph{minimal}  approach for investigating the expressive power and decidability of 
higher-order process calculi.

Our approach is \emph{direct} in that we abandon the idea
of studying the foundations of higher-order concurrency  
by means of translations into first-order languages.
Based on the inadequacy of 
studying higher-order concurrency through first-order translations (as discussed in the previous section), 
we advocate that foundational studies for higher-order process calculi
must be carried out directly on them and exploit their peculiarities.
While we concentrate on expressiveness and decidability issues, this 
direct approach is in concordance with that advocated by 
recent works on other aspects of the theory of higher-order process calculi, such as 
behavioral theory 
(see, e.g., \citep{LSS08,SatoSumii09})
and type systems \citep{Demangeon09}.



On the other hand, our approach is \emph{minimal} in that 
the research shall be centered around a \emph{core calculus} for higher-order concurrency 
in which only the operators strictly necessary to obtain higher-order communication are retained. 
The calculus, called \hocore, aims to be 
the simplest, non-trivial  process calculus featuring higher-order concurrency. 
%Most notably, %
In particular: 
\begin{itemize}
 \item \hocore has \emph{no name-passing}, so processes are the only kind of values that can be passed around in communications.
This is in sharp contrast to most 
%the Higher-Order $\pi$-calculus \citep{San923,SaWabook}, 
higher-order process calculi in the literature,
in which \emph{both} name-passing and process-passing are present. 
% As we mentioned before, the only proposal of higher-order process calculi
% without name passing 
% we are aware of
% is \citep{San96int}.

 \item \hocore has \emph{no restriction operator}, thus all channels are global, and dynamic creation of new channels is impossible.
As such, the behavior of a concurrent system described in \hocore is completely \emph{exposed}.
Also, it is worth noticing that the syntax of higher-order process calculi (including \hocore)
usually omits primitive operators for infinite behavior (as replication), 
as they can be encoded by mimicking the structure of fixed-point combinators in the $\lambda$-calculus. 
Known encodings of fixed-point combinators require restriction; 
therefore, the lack of restriction in \hocore 
is directly related to its ability of expressing infinite behavior. 
While in most of the dissertation 
we consider \hocore (or variants of it) without restriction, 
we shall find it useful to 
consider an extension with 
restriction useful when examining synchronous and polyadic communication.

 \item \hocore has \emph{no output prefix} so it is an \emph{asynchronous} calculus.
It is well-known that asynchronous communication is easier to implement
and maintain
that synchronous communication.
As such, it appears as the \emph{most elemental} communication discipline one could adopt.
Asynchrony represented as the absence of continuations after output actions 
is the main feature of the \emph{asynchronous $\pi$-calculus}, 
which was proposed in seminal papers by \cite{Boudol92} and \cite{HondaT91},
and thoroughly studied since then.
Within concurrency theory, the expressive power of asynchrony has been studied by \cite{Palamidessi03} 
(see also \citep{CacciagranoCP07,BeauxisPV08}), 
who showed that in the $\pi$-calculus 
with choice 
synchronous communication is more expressive than 
asynchronous one. 
Even if the same phenomenon should not necessarily carry over to a higher-order setting
---we shall address this issue in this dissertation---, 
Palamidessi's result ought be taken as an 
additional evidence of the 
simplicity that asynchrony 
might embody in process calculi.
%consequences on expressiveness
%derived from adopting an asynchronous communication discipline.


\end{itemize}

%any first-order features,
%it is asynchronous and lacks a restriction operator.
The minimality of \hocore is convenient in that it allows us 
to focus on  
higher-order communication and its associated phenomena, 
without being shadowed by complex constructs nor by first-order interactions;
studies of expressiveness and decidability for \hocore will therefore reflect the 
inherent to \emph{pure} process passing and shed light on their intrinsic nature.

\subsection{Contributions and Structure}
The dissertation contributes to the theory of higher-order concurrency
with several original results 
on the expressiveness and decidability of \hocore and 
a number of selected variants of it. 
Our results complement the few ones in the literature, and 
deepen and strengthen our understanding of the theory 
core higher-order process calculi as a whole. 
More precisely, our contributions are structured as follows.

\begin{description}
 \item[Chapter \ref{chap:prelim}: Preliminaries.] 
This chapter provides the theoretical background for the thesis.
We introduce fundamental concepts on process calculi, higher-order process calculi,
and expressiveness of concurrent languages.

 \item[Chapter \ref{chap:core}: \hocore and its Expressiveness. ] 
We introduce \hocore, a core calculus for high\-er-order concurrency.
We study the expressive power by encoding basic forms of choice and input-guarded replication.
Such derived constructs are then used to define an encoding of Minsky machines into \hocore, which 
demonstrates that the language is Turing complete.
The encoding is deterministic and termination preserving; 
as such, properties such as \emph{termination} (i.e. the absence of divergent computation)
and \emph{convergence} (i.e. the existence of a non-diverging computation) are 
immediately shown to be undecidable.

%introduces \hocore and analyzes its absolute expressiveness
 \item[Chapter \ref{chap:bt}: Behavioral Theory of \hocore.] We show that 
in \hocore strong bisimilarity is \emph{decidable}. 
To the best of our knowledge, 
\hocore is the first concurrent formalism that is Turing complete 
\emph{and} for which 
bisimilarity is decidable.
Furthermore, strong bisimilarity is shown to be 
a congruence, and 
to coincide with other well-established behavioral equivalences
for higher-order calculi. 
A sound and complete axiomatization of strong bisimilarity is given, and used to 
obtain complexity bounds for bisimilarity checking. 
The limits of decidability are explored by considering an extension of \hocore with static (top-level) restrictions.
For the extension with four of such restrictions, bisimilarity is shown to be
\emph{undecidable}. This result is obtained through an encoding of the Post correspondence problem (PCP).

 \item[Chapter \ref{chap:forward}: Expressiveness of Forwarding and Suspension.] 
We study \hof, the fragment of \hocore that results from forbidding \emph{nested output actions} in communication objects.
This represents a limitation of the \emph{forwarding capabilities} of \hocore.
%, a crucial feature for showing Turing completeness of \hocore. 
The expressiveness of \hof is analyzed using decidability of 
termination %} (i.e. the absence of divergent behavior)
and 
convergence %} (i.e. the existence of a non-diverging computation)
as a yardstick. 
As in \hocore, in \hof convergence is still \emph{undecidable}, a result obtained by exhibiting 
an unfaithful
encoding of Minsky machines. In contrast, termination is shown to be \emph{decidable}.
This result is obtained by appealing to the theory of well-structured transition systems.
To the best of our knowledge, 
 this is the first time such a theory is used in the higher-order setting.

Decidability of termination suggests a loss of expressive power when passing from \hocore to \hof.
Then, as a way of recovering such power, 
we consider 
\hopf, 
the extension of \hof with a \emph{passivation} construct that allows for process \emph{suspension} at run time. 
%\emph{passivation operator}
We show that in \hopf, a faithful encoding of Minsky machines becomes possible. 
This implies that 
in \hopf %the variant with passivation
both
convergence and termination are \emph{undecidable}.
To the best of our knowledge, ours is the first result on the expressiveness 
and decidability of passivation operators in the higher-order setting.


 \item[Chapter \ref{chap:separa}: Expressiveness of Synchronous and Polyadic Communication.] 
We study the expressive power of extensions of \hocore with restriction.
We call such an extension \rhocore. 
As a first encodability result, we show that \rhocore %such an extension 
 is expressive enough to encode \emph{synchronous communication}. 
We then move to study the expressiveness of 
\hopis{n}{×}, 
the extension of \hocore with name restriction, synchronous communication, and 
polyadic communication of arity $n$. 
%polyadic communication in the pure process-passing setting of \hocore. The crucial insight is that in the absence of name-passing, the well-known encoding of polyadic communication into monadic one does not apply. We consider
We consider the family of higher-order process calculi given by varying the polyadicity of such an extension.
The main result is that polyadicity induces a hierarchy of strictly increasing expressiveness:
%in the mentioned family of calculi, 
polyadic communication of arity $n$ 
(as in \hopis{n}{×})
cannot be encoded
into polyadic communication of arity $n-1$ (as in \hopis{n-1}{×}).
Furthermore, we show that 
\bhopis{n}{}
%\shoca 
---the extension of \hopis{n}{×} with 
\emph{abstraction-passing}--- 
cannot be encoded into \hopis{n}{×}.
%is more powerful than polyadic communication of any arity.
%independently of the specific arity.

 \item[Chapter \ref{chap:concl}: Conclusions and Perspectives.] 
We draw conclusions from the research and discuss perspectives of future work.
\end{description}

 \begin{figure}[t]  
 \centering  
    {\includegraphics[width=6.3cm]{./img/languages-1.pdf}}
  \caption[The higher-order process calculi studied in this dissertation]{The higher-order process calculi studied in this dissertation. An arrow indicates language inclusion.}\label{f:languages}
 \end{figure}

The calculi studied in the dissertation are depicted in Figure \ref{f:languages}.

\paragraph{Origin of the Chapters.}
Most of the material in this dissertation has been previously 
presented in international conferences and appear in the respective proceedings.
Even if many improvements have been made with respect to the 
published material, we think that the basic ideas behind the results remain the same.

\begin{itemize}
 \item \hocore and its behavioral theory as presented in Chapters \ref{chap:core} and \ref{chap:bt}
has been published as the paper \citep{LanesePSS08}.

\item The expressiveness of forwarding in \hocore, as presented in Chapter \ref{chap:forward}, 
is based on results first published in the paper \citep{GiustoPZ09}.

\item The expressiveness of polyadic communication as discussed in Chapter \ref{chap:separa}
is based on results published as the extended abstract \citep{LanesePSS09}.
\end{itemize}

There are some results original to this dissertation;
this unpublished material will be explicitly mentioned in the corresponding chapter.






% Chapters \ref{chap:core} and \ref{chap:bt} are based on the paper \cite{LanesePSS08}.
% 
% Chapter \ref{chap:forward} is mostly based on the paper \cite{GiustoPZ09}.
% 
% Chapter \ref{chap:separa} is the long version of an extended abstract published as \cite{LanesePSS09}.



% \section{Higher-Order Languages for Concurrency}
% \section{Expressiveness of Concurrent Languages}
% \section{Contributions}
% \section{Organization}